{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses,
  FlexibleContexts, UndecidableInstances, Rank2Types, TemplateHaskell,
  TypeFamilies #-}

{- |

Module      :  Data.Yoko.InDT
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Various type sets determined by a data constructor type's suitability to be
embedded in a data type.

-}
module Data.Yoko.InDT where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect



-- | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@
-- constructor satisfying @'TagRepIs' tag c@.
data HasTagRepU tag c t where
  HasTagRepU ::
    DT t => SuchThat (DCs t) (TagRepIs tag c) -> HasTagRepU tag c t
obvious_membership ''HasTagRepU

instance SetModel (HasTagRepU tag c) where
  evidence (HasTagRepU (u, v@TagRepIs)) x = evidence u $ evidence v x

-- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into
-- @t@.
hasTagRepU :: HasTagRepU tag c t -> RMI c -> t
hasTagRepU (HasTagRepU (u, TagRepIs)) = case weaken u of
  DCSet -> fr_DCOf u . obj





-- | Often times, we're interested in the set of types accomodating a data
-- constructor's image under some type-function.
type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))

-- | A constructor type @dc@ inhabits @ImageHasTagRepU t fn@ if
--
-- 1. @fn@ can be mapped across the recursive occurrences in @dc@, and
--
-- 2. @t@ has a constructor isomorphic to the @fn@-image of @dc@ 
data ImageInDTU t fn dc where
  ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
                ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc
obvious_membership ''ImageInDTU

instance SetModel (ImageInDTU t fn) where
  evidence (ImageInDTU u) x = evidence u x

-- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be
-- embedded into @t@.
imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t
imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep

-- | Same as @ImageInDTD@, but uses an implicitly applicative function.
data ImageAInDTU t fn dc where
  ImageAInDTU :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)
                 ) => HasTagRepImageU (fn IdM) dc t -> ImageAInDTU t fn dc
obvious_membership ''ImageAInDTU

instance SetModel (ImageAInDTU t fn) where
  evidence (ImageAInDTU u) x = evidence u x

imageAInDTU :: Functor (Idiom (fn IdM)) =>
               (forall t. fn IdM t) -> ImageAInDTU t fn dc -> RMNI dc -> Idiom (fn IdM) t
imageAInDTU fn (ImageAInDTU d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep
